BEGIN

EVAL '(DECLARE (DECIMAL) (SPECIAL AXIOMS CURLIN CURPRF PROOFS SCHEMAS THEOREMS) (SPECIAL LOGICALCONSTANTS 
	QUANTIFIERS) (SPECIAL EXPEXP EXPLGTH EXPLIM ORDCNT) (SPECIAL CONSOLEWIDTH DDWIDTH FILEWIDTH IIIWIDTH 
	IMLACWIDTH TTYWIDTH) (SPECIAL ?*FILEPRINT PRECLIS?* ?*PRINT ?*TWODIM));


MACRO FIRSTPROP (L);
	'CDR CONS CDR L;


MACRO LASTPROP (L);
	'NULL CONS CDR L;


MACRO NEXTPROP (L);
	'CDDR CONS CDR L;


MACRO PROPNAM (L);
	'CAR CONS CDR L;


MACRO PROPTABLE (L);
	'CDR CONS CDR L;


MACRO PROPVAL (L);
	'CADR CONS CDR L;


EXPR DELETEPROP (IDENT, PROPNAM);
	BEGIN
	NEW TEM;
	TEM ← IDENT;
LOOP; 	IF NULL CDR TEM THEN RETURN NIL;
	IF TEM[2] EQ PROPNAM THEN RETURN PROG2(RPLACD(TEM, CDDDR TEM), T);
	TEM ← CDDR TEM;
	GO LOOP;
	END;


EXPR GETGET (ATOM
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  ATOM
                 , PROP);
	BEGIN
	NEW TEM, PTAB;
	PTAB ← CDR ATOM
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  ATOM
                       ;
LOOP; 	IF NULL PTAB THEN RETURN NIL;
	TEM ← SEEKPROP(CAR PTAB, PROP);
	IF ¬NULL TEM THEN RETURN TEM;
	PTAB ← CDDR PTAB;
	GO LOOP;
	END;


EXPR INITPROP (IDENT, VALUE, NAME);
	RPLACD(IDENT, NAME CONS VALUE CONS CDR IDENT);


EXPR SEEKPROP (IDENT, PROPNAM);
	BEGIN
	NEW TEM;
	TEM ← GETL(IDENT, <PROPNAM>);
	IF NULL TEM THEN RETURN NIL;
	RETURN TEM;
	END;


FEXPR AE (ARGS);
	BEGIN
	NEW WFF;
	WFF ← WFFPART(CAR ARGS);
	IF CAR WFF ≠ 'AND THEN ERREND('(FIRST ARG IS NOT AN AND));
	ADDLINE(ANDELIM1(WFF, CDR ARGS), 'AE CONS ARGS, ASSPART(CAR ARGS));
	END;


FEXPR AI (ARGS);
	ADDLINE(CONJOIN(WFFLIST(ARGS)), 'AI CONS ARGS, UNION(ASSLIST(ARGS)));


FEXPR ALT (ARGS);
	BEGIN
	NEW NEWEXP;
	NEWEXP ← ALT1(WFFPART(CAR ARGS), WFFPART(ARGS[2]));
	IF ¬VALID(NEWEXP) THEN ERREND('(LINES ARE NOT ALTERNATIVES));
	ADDLINE(NEWEXP, <'ALT CONS ARGS>, UNION2(ASSPART(CAR ARGS), ASSPART(ARGS[2])));
	END;


FEXPR ASS (PROP);
	ADDLINE(CAR PROP, 'ASS CONS PROP, <NEXTLINE()>);


FEXPR BS (ARGS);
	ADDLINE(BOUNDSUBST(WFFPART(CAR ARGS), MAKECONSES(CDR ARGS), NIL), 'BS CONS ARGS, ASSPART(CAR ARGS));


FEXPR DED (LINES);
	BEGIN
	IF NULL LINES THEN ERREND('(NOTHING TO CONCLUDE));
	ADDLINE(<'IMPLIES, CONJOIN(WFFLIST(CDR LINES)), WFFPART(CAR LINES)>, 'DED CONS LINES, SETDIF(ASSPART(
		CAR LINES), CDR LINES));
	END;


FEXPR DEF (ARGS);
	BEGIN
	IF ¬ATOM CAR ARGS THEN ERREND('(NAMES MUST BE ATOMS));
	ADDLINE('SETQ CONS ARGS, 'DEF CONS ARGS, <NEXTLINE()>);
	END;


FEXPR DNE (LINE);
	BEGIN
	NEW NEWSTAT;
	IF ¬VALID(NEWSTAT ← DOUBLENEG(WFFPART(CAR LINE))) THEN ERREND('(NO DOUBLE NEGATIVE));
	ADDLINE(NEWSTAT, 'DNE CONS LINE, ASSPART(CAR LINE));
	END;


FEXPR DNI (LINE);
	ADDLINE(<'NOT, <'NOT, WFFPART(CAR LINE)>>, 'DNI CONS LINE, ASSPART(CAR LINE));


FEXPR EG (ARGS);
	ADDLINE(EXGEN1(WFFPART(CAR ARGS), CDR ARGS), 'EG CONS ARGS, ASSPART(CAR ARGS));


FEXPR ELIM (ARGS);
	BEGIN
	NEW NEW
*** WARNING, MLISP RESERVED WORD:  NEW
               ;
	NEW
*** WARNING, MLISP RESERVED WORD:  NEW
            ← WFFPART(ARGS[2]);
	IF CAR NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                   ≠ 'SETQ THEN ERREND('(NO DEFINITION));
	ADDLINE(SUBST(NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                         [3], NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                                 [2], WFFPART(CAR ARGS)), 'ELIM CONS ARGS, SETDIF(ASSPART(CAR ARGS), ASSPART(
		ARGS[2])));
	END;


FEXPR EQE (ARGS);
	BEGIN
	NEW NEW
*** WARNING, MLISP RESERVED WORD:  NEW
               ;
	NEW
*** WARNING, MLISP RESERVED WORD:  NEW
            ← WFFPART(CAR ARGS);
	IF CAR NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                   ≠ 'EQUIVALENT THEN ERREND('(NO EQUIVALENCE));
	NEW
*** WARNING, MLISP RESERVED WORD:  NEW
            ← 	IF ARGS[2] = 2 THEN REVERSE CDR NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                                                   
		ELSE CDR NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                            ;
	ADDLINE('IMPLIES CONS NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                                 , 'EQE CONS ARGS, ASSPART(CAR ARGS));
	END;


FEXPR EQI (ARGS);
	BEGIN
	NEW NEW
*** WARNING, MLISP RESERVED WORD:  NEW
               ;
	IF ¬VALID(NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                      ← EQI1(WFFPART(CAR ARGS), WFFPART(CAR ARGS))) THEN ERREND('(ARE NOT EQUIVALENT));
	ADDLINE(NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                   , 'EQI CONS ARGS, UNION2(ASSPART(CAR ARGS), ASSPART(ARGS[2])));
	END;


FEXPR ES (ARGS);
	ADDLINE(SPECALL(WFFPART(CAR ARGS), CDR ARGS), 'ES CONS ARGS, ASSPART(CAR ARGS));


FEXPR IFE (ARGS);
	BEGIN
	NEW NEW
*** WARNING, MLISP RESERVED WORD:  NEW
               ;
	IF ¬VALID(NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                      ← IFE1(WFFPART(CAR ARGS), WFFPART(ARGS[2]))) THEN 
		ERREND('(NO IF ?- THEN ?- ELSE EXPRESSION));
	ADDLINE(NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                   , 'IFE CONS ARGS, UNION2(ASSPART(CAR ARGS), ASSPART(ARGS[2])));
	END;


FEXPR IFI (ARGS);
	BEGIN
	NEW NEW
*** WARNING, MLISP RESERVED WORD:  NEW
               ;
	IF ¬VALID(NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                      ← IFI1(WFFPART(CAR ARGS), WFFPART(ARGS[2]))) THEN 
		ERREND('(NEED IMPLICATIONS WITH OPPOSITE ANTECEDENTS));
	ADDLINE(NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                   , 'IFI CONS ARGS, UNION2(ASSPART(CAR ARGS), ASSPART(ARGS[2])));
	END;


FEXPR LC (ARGS);
	ADDLINE(<'EQUAL, ARGS, LAMEXP(ARGS)>, 'LC CONS ARGS, NIL);


FEXPR MP (ARGS);
	BEGIN
	NEW NEWSTAT;
	IF ¬VALID(NEWSTAT ← MP1(WFFPART(CAR ARGS), WFFPART(ARGS[2]))) THEN 
		ERREND('(CANNOT MODUS PONENS));
	ADDLINE(NEWSTAT, 'MP CONS ARGS, UNION2(ASSPART(CAR ARGS), ASSPART(ARGS[2])));
	END;


FEXPR NE (ARGS);
	BEGIN
	IF ¬VALID(NOTELIM(WFFPART(CAR ARGS), WFFPART(ARGS[2]))) THEN ERREND('(NO CONTRADICTION));
	ADDLINE('FALSE, 'NE CONS ARGS, UNION2(ASSPART(CAR ARGS), ASSPART(ARGS[2])));
	END;


FEXPR NI (IM);
	BEGIN
	NEW NEWSTAT;
	IF ¬VALID(NEWSTAT ← NOTINTRO(WFFPART(CAR IM))) THEN ERREND('(NO IMPLIES FALSE));
	ADDLINE(NEWSTAT, 'NI CONS IM, ASSPART(CAR IM));
	END;


FEXPR OE (ARGS);
	BEGIN
	IF NULL ARGS | NULL CDR ARGS THEN ERREND('(NEED AT LEAST TWO ARGS));
	ADDLINE(ORELIM1(WFFPART(CAR ARGS), WFFLIST(CDR ARGS)), 'OE CONS ARGS, UNION(ASSLIST(ARGS)));
	END;


FEXPR OI (ARGS);
	BEGIN
	NEW KNOWN, SAVARGS, WFFS;
	SAVARGS ← ARGS;
LOOP; 	IF NULL ARGS THEN 
		IF NULL KNOWN THEN ERREND('(NO VALID PROPOSITION))
		ELSE GO ADDL;
	IF NUMBERP CAR ARGS THEN 
		(IF NULL KNOWN THEN KNOWN ← CAR ARGS);
	IF NUMBERP CAR ARGS THEN WFFS ← WFFPART(CAR ARGS) CONS WFFS
	ELSE WFFS ← CAR ARGS CONS WFFS;
	ARGS ← CDR ARGS;
	GO LOOP;
ADDL; 	ADDLINE(IF NULL CDR WFFS THEN CAR WFFS
		ELSE 'OR CONS REVERSE WFFS, 'OI CONS SAVARGS, ASSPART(KNOWN));
	END;


FEXPR REP (ARGS);
	BEGIN
	NEW NEW
*** WARNING, MLISP RESERVED WORD:  NEW
               ;
	NEW
*** WARNING, MLISP RESERVED WORD:  NEW
            ← WFFPART(ARGS[2]);
	IF ¬ISEQUIVALENCE(CAR NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                                 ) THEN ERREND('(NO EQUATION));
	NEW
*** WARNING, MLISP RESERVED WORD:  NEW
            ← 	IF ARGS[3] = 2 THEN REVERSE CDR NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                                                   
		ELSE CDR NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                            ;
	ADDLINE(SUBST(NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                         [2], CAR NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                                     , WFFPART(CAR ARGS)), 'REP CONS ARGS, UNION2(ASSPART(CAR ARGS), ASSPART(
		ARGS[2])));
	END;


FEXPR REPL (ARGS);
	ADDLINE(REPEITHER(WFFPART(CAR ARGS), WFFPART(ARGS[2]), T, ARGS[3]), 'REPL CONS ARGS, UNION2(ASSPART(CAR
		 ARGS), ASSPART(ARGS[2])));


FEXPR REPR (ARGS);
	ADDLINE(REPEITHER(WFFPART(CAR ARGS), WFFPART(ARGS[2]), NIL, ARGS[3]), 'REPR CONS ARGS, UNION2(ASSPART
		(CAR ARGS), ASSPART(ARGS[2])));


FEXPR TAUT (L);
	BEGIN
	IF ¬TH1(NIL, NIL, WFFLIST(CDR L), <CAR L>) THEN ERREND('(DOES NOT FOLLOW));
	ADDLINE(CAR L, 'TAUT CONS L, UNION(ASSLIST(CDR L)));
	END;


FEXPR UG (ARGS);
	BEGIN
	NEW ASS, VARS, WFF;
	WFF ← WFFPART(CAR ARGS);
	ASS ← ASSPART(CAR ARGS);
	VARS ← CDR ARGS;
LOOP; 	IF NULL VARS THEN GO ADDL;
	IF ATOM CAR VARS THEN GO ATOM
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  ATOM
                                     ;
	IF VARS[1,1] = 'CONS THEN GO DOT;
	ERREND('(ILLEGAL ARGUMENT));
ATOM
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  ATOM
    ; 	WFF ← UNGEN(WFF, ASS, CAR VARS, CAR VARS);
	GO ELOOP;
DOT; 	WFF ← UNGEN(WFF, ASS, VARS[1,2], VARS[1,3]);
ELOOP; 	VARS ← CDR VARS;
	GO LOOP;
ADDL; 	ADDLINE(WFF, 'UG CONS ARGS, ASSPART(CAR ARGS));
	END;


FEXPR US (ARGS);
	BEGIN
	ADDLINE(SPECALL(WFFPART(CAR ARGS), CDR ARGS), 'US CONS ARGS, ASSPART(CAR ARGS));
	END;


FEXPR USEAX (ARGS);
	BEGIN
	NEW AX, FORM;
	AX ← GET(CAR ARGS, 'AXIOM);
	IF NULL AX THEN ERREND('(NO SUCH AXIOM));
	FORM ← SPECALL(AX, CDR ARGS);
	ADDLINE(FORM, 'USEAX CONS ARGS, NIL);
	END;


FEXPR USESCHM (ARGS);
	BEGIN
	NEW SCHEMA;
	SCHEMA ← GET(CAR ARGS, 'SCHEMA);
	IF NULL SCHEMA THEN ERREND('(IS NOT SCHEMA));
	ADDLINE(LAMEXP(PROPSUBST(ARGS[2], SCHEMA[1,2], SCHEMA[2])), 'USESCHM CONS ARGS, NIL);
	END;


FEXPR USETHM (ARGS);
	BEGIN
	NEW TH, FORM;
	TH ← GET(CAR ARGS, 'THEOREM);
	IF NULL TH THEN ERREND('(NO SUCH THEOREM));
	FORM ← SPECALL(TH, CDR ARGS);
	ADDLINE(FORM, 'USETHM CONS ARGS, NIL);
	END;


FEXPR BT (LINO);
	BEGIN
	NEW PROOF;
	LINO ← 	IF NULL LINO THEN CURLINE() - 1
		ELSE CAR LINO;
	PROOF ← CURTEXT();
	IF LINO ?*GREAT CURLINE() | LINO ?*LESS 0 THEN ERREND('(NON EXISTANT LINE));
	IF LINO = 0 THEN PUTPROP(CURPROOF(), NIL, 'PROOF)
	ELSE 	BEGIN
		RPLACD(NTHCDR(PROOF, LINO - 1), NIL);
		PUTPROP(CURPROOF(), PROOF, 'PROOF);
		END;
	INITPROOF(CURPROOF());
	SHOWCURLINE();
	END;


FEXPR FINDL (L);
	BEGIN
	NEW PRF, TXT, WFF;
	WFF ← CAR L;
	PRF ← 	IF ¬NULL CDR L THEN L[2]
		ELSE CURPROOF();
	TXT ← GET(PRF, 'PROOF);
LOOP; 	IF NULL TXT THEN RETURN NIL;
	IF WFF = TXT[1,2] THEN SHOWLINE(CAR TXT);
	TXT ← CDR TXT;
	GO LOOP;
	END;


FEXPR GIVEAX (L);
	BEGIN
	IF ¬ATOM CAR L THEN ERREND('(NON ATOMIC AXIOM NAME));
	IF ¬(CAR L ε AXIOMS) THEN AXIOMS ← AXIOMS @ <CAR L>;
	PUTPROP(CAR L, L[2], 'AXIOM);
	IF ?*PRINT THEN SHOWAXIOM(CAR L);
	END;


FEXPR GIVESCHM (L);
	BEGIN
	IF ¬ATOM CAR L THEN ERREND('(NON ATOMIC SCHEMA NAME));
	IF ¬(CAR L ε SCHEMAS) THEN SCHEMAS ← SCHEMAS @ <CAR L>;
	PUTPROP(CAR L, L[2], 'SCHEMA);
	IF ?*PRINT THEN SHOWSCHEMA(CAR L);
	END;


EXPR INVENTORY ();
	BEGIN
	IF ¬NULL AXIOMS THEN 
		BEGIN
		TERPRI();
		PRINT 'AXIOMS;
		PRINL(AXIOMS);
		END;
	IF ¬NULL SCHEMAS THEN 
		BEGIN
		TERPRI();
		PRINT 'SCHEMAS;
		PRINL(SCHEMAS);
		END;
	IF ¬NULL PROOFS THEN 
		BEGIN
		TERPRI();
		PRINT 'PROOFS;
		PRINL(PROOFS);
		END;
	IF ¬NULL THEOREMS THEN 
		BEGIN
		TERPRI();
		PRINT 'THEOREMS;
		PRINL(THEOREMS);
		END;
	END;


FEXPR MAKETHM (ARG
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  ARG
                  );
	MAKETHEOREM1(CAR ARG
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  ARG
                            , ARG
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  ARG
                                 [2], 
		IF ¬NULL CDDR ARG
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  ARG
                                  THEN ARG
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  ARG
                                          [3]
		ELSE CURPROOF());


EXPR ONDD ();
	BEGIN
	INITSTANCHARSET();
	LINELENGTH (CONSOLEWIDTH ← DDWIDTH);
	END;


EXPR ONIII ();
	BEGIN
	INITSTANCHARSET();
	LINELENGTH (CONSOLEWIDTH ← IIIWIDTH);
	END;


EXPR ONIMLAC ();
	BEGIN
	INITSTANCHARSET();
	LINELENGTH (CONSOLEWIDTH ← IMLACWIDTH);
	END;


EXPR ONTTY ();
	BEGIN
	INITTTYCHARSET();
	LINELENGTH (CONSOLEWIDTH ← TTYWIDTH);
	END;


FEXPR PROOF (NAME);
	BEGIN
	IF NULL NAME THEN ERREND('(NO NAME GIVEN));
	IF ¬ATOM CAR NAME THEN ERREND('(NON ATOMIC PROOF NAME));
	INITPROOF(CAR NAME);
	IF ?*PRINT THEN SHOWCURLINE();
	END;


FEXPR REDO (ARGS);
	BEGIN
	NEW CHANGED, CURL, LASTL, NEWC;
	IF WFFPART(CAR ARGS) ≠ WFFPART(ARGS[2]) THEN ERREND('(CANNOT REDO));
	CHANGED ← (CAR ARGS CONS ARGS[2]) CONS NIL;
	CURL ← CAR ARGS + 1;
	LASTL ← CURLINE() + 1;
LOOP; 	IF CURL EQ LASTL THEN RETURN NIL;
	NEWC ← SUBLIS(CHANGED, BYPART(CURL));
	IF NEWC = BYPART(CURL) THEN GO ELOOP
	ELSE EVAL NEWC;
	CHANGED ← (CURL CONS CURLINE()) CONS CHANGED;
ELOOP; 	CURL ← CURL + 1;
	GO LOOP;
	END;


FEXPR RESTOREALL (FILES);
	BEGIN
	NEW DEV, FILE, ?*PRINT;
	IF ?*FILEPRINT THEN 
		BEGIN
		?*PRINT ← T;
		END;
	DEV ← 'DSK;
LOOP; 	IF NULL FILES THEN GO EXIT;
	FILE ← CAR FILES;
	IF ATOM FILE THEN GO READ;
	IF CAR FILE = 'QUOTE THEN GO DEVICE;
	IF CAR FILE = 'CONS THEN GO DOTTED;
	ERREND('(NOT FILE OR DEVICE NAME));
READ; 	READIN(DEV, <FILE>, NIL);
	GO ELOOP;
DOTTED; 	FILE ← FILE[2] CONS FILE[3];
	GO READ;
DEVICE; 	DEV ← FILE[2];
	GO ELOOP;
ELOOP; 	FILES ← CDR FILES;
	GO LOOP;
EXIT; 	INVENTORY();
	END;


FEXPR SAVEALL (FILE);
	BEGIN
	NEW DEV, ITEM;
	DEV ← 'DSK;
LOOP; 	IF NULL FILE THEN ERREND('(DEVICE BUT NO FILE));
	ITEM ← CAR FILE;
	IF ATOM ITEM THEN GO OUTPUT;
	IF CAR ITEM = 'QUOTE THEN GO DEVICE;
	IF CAR ITEM = 'CONS THEN GO DOTTED;
	ERREND('(NOT FILE SPECIFIER));
DEVICE; 	DEV ← ITEM[2];
	FILE ← CDR FILE;
	GO LOOP;
DOTTED; 	ITEM ← ITEM[2] CONS ITEM[3];
OUTPUT; 	EVAL <'OUTPUT, DEV, ITEM>;
	OUTC(T, NIL);
	LINELENGTH FILEWIDTH;
	MAPC(FUNCTION(SAVEAXIOM), AXIOMS);
	MAPC(FUNCTION(SAVESCHEMA), SCHEMAS);
	MAPC(FUNCTION(SAVEPROOF), PROOFS);
	MAPC(FUNCTION(SAVETHEOREM), THEOREMS);
	OUTC(NIL, T);
	INVENTORY();
	END;


FEXPR SAVECOMS (FILE);
	BEGIN
	NEW DEV, ITEM;
	DEV ← 'DSK;
LOOP; 	IF NULL FILE THEN ERREND('(NO FILE SPECIFIED));
	ITEM ← CAR FILE;
	IF ATOM ITEM THEN GO OUTPUT;
	IF CAR ITEM = 'QUOTE THEN GO DEVICE;
	IF CAR ITEM = 'CONS THEN GO DOTTED;
	ERREND('(NOT FILE SPECIFIER));
DEVICE; 	DEV ← ITEM[2];
	FILE ← CDR FILE;
	GO LOOP;
DOTTED; 	ITEM ← ITEM[2] CONS ITEM[3];
OUTPUT; 	EVAL <'OUTPUT, DEV, ITEM>;
	OUTC(T, NIL);
	LINELENGTH FILEWIDTH;
	MAPC(FUNCTION(SAVEAXCOM), AXIOMS);
	MAPC(FUNCTION(SAVESCHMCOM), SCHEMAS);
	MAPC(FUNCTION(SAVEPRFCOM), PROOFS);
	MAPC(FUNCTION(SAVETHMCOM), THEOREMS);
	OUTC(NIL, T);
	INVENTORY();
	END;


FEXPR SHOW (THINGS);
	BEGIN
	NEW LINE1, LINE2, TEM;
TOP; 	IF NULL THINGS THEN RETURN SHOWPROOF(CURPROOF());
LOOP; 	IF NULL THINGS THEN GO EXIT;
	IF ¬ATOM CAR THINGS THEN GO DEV;
	IF NUMBERP CAR THINGS THEN GO LINES;
	TEM ← GETGET(CAR THINGS, 'IMAGE);
	IF NULL TEM THEN ERREND('(NOTHING TO SHOW));
	EVAL '((CADR TEM) (CAR THINGS));
ELOOP; 	THINGS ← CDR THINGS;
	GO LOOP;
LINES; 	LINE1 ← CAR THINGS;
	THINGS ← CDR THINGS;
	IF NULL THINGS | ¬NUMBERP CAR THINGS THEN LINE2 ← LINE1
	ELSE 	BEGIN
		LINE2 ← CAR THINGS;
		THINGS ← CDR THINGS;
		END;
LLOOP; 	IF LINE1 ?*GREAT LINE2 THEN GO EXIT;
	SHOWLINE(GETLINE(LINE1));
	LINE1 ← LINE1 + 1;
	GO LLOOP;
DEV; 	IF THINGS[1,1] ≠ 'QUOTE THEN ERREND('(NEED NAME OR FILE SPEC));
	EVAL ('OUTPUT CONS THINGS[1,2]);
	OUTC(T, T);
	THINGS ← CDR THINGS;
	GO TOP;
EXIT; 	OUTC(NIL, T);
	END;


FEXPR SHOWALL (FILE);
	BEGIN
	NEW DEV, ITEM;
	DEV ← 'DSK;
LOOP; 	IF NULL FILE THEN ERREND('(NO FILE SPECIFIED));
	ITEM ← CAR FILE;
	IF ATOM ITEM THEN GO OUTPUT;
	IF CAR ITEM = 'QUOTE THEN GO DEVICE;
	IF CAR ITEM = 'CONS THEN GO DOTTED;
	ERREND('(NOT FILE SPECIFIER));
DEVICE; 	DEV ← ITEM[2];
	FILE ← CDR FILE;
	GO LOOP;
DOTTED; 	ITEM ← ITEM[2] CONS ITEM[3];
OUTPUT; 	EVAL <'OUTPUT, DEV, ITEM>;
	OUTC(T, NIL);
	LINELENGTH FILEWIDTH;
	MAPC(FUNCTION(SHOWAXIOM), AXIOMS);
	MAPC(FUNCTION(SHOWSCHEMA), SCHEMAS);
	MAPC(FUNCTION(SHOWPROOF), PROOFS);
	MAPC(FUNCTION(SHOWTHEOREM), THEOREMS);
	OUTC(NIL, T);
	INVENTORY();
	END;


FEXPR SSEX (L);
	BEGIN
	NEW LINE, NAME, PRF;
	NAME ← 	IF NULL L THEN CURPROOF()
		ELSE CAR L;
	PRF ← GETL(NAME, '(PROOF));
	IF NULL PRF THEN ERREND('(NO PROOF BY THAT NAME));
	PRF ← PRF[2];
	PRINT 'PROOF;
	PRINS(NAME);
LOOP; 	IF NULL PRF THEN RETURN NIL;
	LINE ← CAR PRF;
	TERPRI();
	PRINC CAR LINE;
	PRINC '?/;
	PRINTSUBEXPR(LINE[2], CURCOL(), 0);
	IF FLATSIZE CDDR LINE + 6 ?*GREAT CHRCT() THEN GO MANY;
	PRINC '?/;
	PRINS('BY);
	PRINS(LINE[3]);
	IF ¬NULL LINE[4] THEN 
		BEGIN
		PRINS('ASS);
		PRIN1 LINE[4];
		END;
ELOOP; 	PRF ← CDR PRF;
	GO LOOP;
MANY; 	TERPRI();
	PRINTN('?/, 4);
	PRINC 'BY;
	PRINC '?/;
	PRINTSUBEXPR(LINE[3], CURCOL(), 0);
	IF NULL LINE[4] THEN GO ELOOP;
	TERPRI();
	PRINTN('?/, 4);
	PRINC 'ASS;
	PRINC '?/;
	PRINS(LINE[4]);
	GO ELOOP;
	END;


EXPR ADDLINE (WFF, JUST, ASS);
	BEGIN
	PUTPROP(CURPROOF(), CURTEXT() NCONC <<CURLINE() + 1, WFF, JUST, ASS>>, 'PROOF);
	CURLIN ← CURLIN + 1;
	PUTPROP('?@, CURLINE(), 'NEWNAM);
	IF ?*PRINT THEN SHOWCURLINE();
	END;


FEXPR ADDAXIOM (L);
	BEGIN
	PUTPROP(CAR L, L[2], 'AXIOM);
	AXIOMS ← CAR L CONS AXIOMS;
	END;


FEXPR ADDSCHEMA (L);
	BEGIN
	PUTPROP(CAR L, L[2], 'SCHEMA);
	SCHEMAS ← CAR L CONS SCHEMAS;
	END;


FEXPR ADDTHEOREM (L);
	BEGIN
	PUTPROP(CAR L, L[2], 'THEOREM);
	THEOREMS ← CAR L CONS THEOREMS;
	END;


EXPR ALPHAPART (IDENT);
	BEGIN
	NEW CHARS;
	CHARS ← REVERSE EXPLODE IDENT;
LOOP; 	IF ¬NUMBERP CAR CHARS THEN RETURN READLIST REVERSE CHARS;
	CHARS ← CDR CHARS;
	GO LOOP;
	END;


EXPR ALLVARS (EXPRESSION);
	ALLVARS1(EXPRESSION, NIL);


EXPR ALLVARS1 (EXP, VARS);
	IF ATOM EXP THEN 
		IF ISVAR(EXP) THEN 
			IF EXP ε VARS THEN VARS
			ELSE EXP CONS VARS
		ELSE VARS
	ELSE ALLVARSL(CDR EXP, VARS);


EXPR ALLVARSL (EXPL, VARS);
	IF NULL EXPL THEN VARS
	ELSE ALLVARS1(CAR EXPL, ALLVARSL(CDR EXPL, VARS));


EXPR ALT1 (I1, I2);
	LAMBDA (U, V); 
		IF VALID(U) THEN SUBLIS(U, 'QQQ)
		ELSE IF VALID(V) THEN SUBLIS(V, 'QQQ)
		ELSE 'INVALID;
	(INST(I1 CONS I2, '((IMPLIES PPP QQQ) IMPLIES (NOT PPP) QQQ), NIL), INST(I2 CONS I1, '((IMPLIES PPP QQQ
		) IMPLIES (NOT PPP) QQQ), NIL));


EXPR ANDELIM1 (WFF, PLACES);
	BEGIN
	NEW CHOSEN, LEN;
	LEN ← LENGTH CDR WFF;
	IF CAR WFF NEQ 'AND THEN ERREND('(FIRST ARG IS NOT AN AND));
LOOP; 	IF NULL PLACES THEN RETURN CONJOIN(REVERSE CHOSEN);
	IF CAR PLACES ?*GREAT LEN THEN ERREND('(TOO FEW CONJUNCTS));
	CHOSEN ← NTHELT(CDR WFF, CAR PLACES) CONS CHOSEN;
	PLACES ← CDR PLACES;
	GO LOOP;
	END;


EXPR ASSLIST (L);
	MAPCAR(FUNCTION(ASSPART), L);


EXPR ASSOCR (ITM, LST);
	BEGIN
LOOP; 	IF NULL LST THEN RETURN NIL;
	IF ITM EQ CDAR LST THEN RETURN CAR LST;
	LST ← CDR LST;
	GO LOOP;
	END;


EXPR ASSPART (LINE);
	GETLINE(LINE)[4];


EXPR BINAND (ARGS);
	IF NULL ARGS THEN '(AND TRUE TRUE)
	ELSE IF NULL CDR ARGS THEN <'AND, CAR ARGS, 'TRUE>
	ELSE IF NULL CDDR ARGS THEN 'AND CONS ARGS
	ELSE <'AND, CAR ARGS, BINAND(CDR ARGS)>;


EXPR BINOR (ARGS);
	IF NULL ARGS THEN '(OR FALSE FALSE)
	ELSE IF NULL CDR ARGS THEN <'OR, CAR ARGS, 'FALSE>
	ELSE IF NULL CDDR ARGS THEN 'OR CONS ARGS
	ELSE <'OR, CAR ARGS, BINOR(CDR ARGS)>;


EXPR BYPART (LINE);
	GETLINE(LINE)[3];


EXPR BOUNDSUBST (EXP, SUBS, BINDS);
	BEGIN
	NEW TEM;
	IF ATOM EXP THEN GO ATOM
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  ATOM
                                ;
	IF ISQUANT(EXP[1,1]) THEN GO QUANT;
	RETURN BOUNDSUBSTL(EXP, SUBS, BINDS);
ATOM
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  ATOM
    ; 	IF ISCONST(EXP) THEN RETURN EXP;
	TEM ← ASSOC(EXP, BINDS);
	IF ¬NULL TEM THEN RETURN CDR TEM;
	TEM ← ASSOCR(EXP, BINDS);
	IF ¬NULL TEM THEN ERREND('(FREE VARIABLE CAPTURE));
	RETURN EXP;
QUANT; 	TEM ← ASSOC(EXP[1,2], SUBS);
	TEM ← 	IF ¬NULL TEM THEN CDR TEM
		ELSE EXP[1,2];
	IF ¬NULL ASSOCR(TEM, BINDS) THEN ERREND('(BOUND VARIABLE CAPTURE));
	RETURN <<EXP[1,1], TEM>, BOUNDSUBST(EXP[2], SUBS, (EXP[1,2] CONS TEM) CONS BINDS)>;
	END;


EXPR BOUNDSUBSTL (LST, SUBS, BINDS);
	IF NULL LST THEN NIL
	ELSE BOUNDSUBST(CAR LST, SUBS, BINDS) CONS BOUNDSUBSTL(CDR LST, SUBS, BINDS);


EXPR CONJOIN (WFFS);
	IF NULL WFFS THEN 'TRUE
	ELSE IF NULL CDR WFFS THEN CAR WFFS
	ELSE 'AND CONS WFFS;


EXPR CURCOL ();
	LINELENGTH NIL + (1 - CHRCT());


EXPR CURLINE ();
	PROG2(CURPROOF(), CURLIN);


EXPR CURPROOF ();
	IF NULL CURPRF THEN ERREND('(NO CURRENT PROOF))
	ELSE CURPRF;


EXPR CURTEXT ();
	GET(CURPROOF(), 'PROOF);


EXPR DOUBLENEG (PROP);
	LAMBDA (W); 
		IF ¬VALID(W) THEN 'INVALID
		ELSE SUBLIS(W, 'PPP);
	(INST(PROP, '(NOT (NOT PPP)), NIL));


EXPR EXGEN1 (WFF, VARS);
	BEGIN
LOOP; 	IF NULL VARS THEN RETURN WFF;
	IF ATOM CAR VARS THEN GO ATOM
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  ATOM
                                     ;
	IF VARS[1,1] = 'CONS THEN GO DOT;
	ERREND('(ILLEGAL ARGUMENT));
ATOM
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  ATOM
    ; 	WFF ← EXGEN(WFF, CAR VARS, CAR VARS);
	GO ELOOP;
DOT; 	WFF ← EXGEN(WFF, VARS[1,2], VARS[1,3]);
ELOOP; 	VARS ← CDR VARS;
	GO LOOP;
	END;


EXPR EXGEN (WFF, OLD, NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                         );
	BEGIN
	NEW TEM;
	TEM ← GENSYM();
	WFF ← SUBST(TEM, OLD, WFF);
	IF NEW
*** WARNING, MLISP RESERVED WORD:  NEW
               ε ALLVARS(WFF) THEN ERREND('(NEW VARIABLE CONFLICTS));
	RETURN <<'THEREEXISTS, NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                                  >, SUBST(NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                                              , TEM, WFF)>;
	END;


EXPR EQI1 (WFF1, WFF2);
	LAMBDA (W); 
		IF ¬VALID(W) THEN 'INVALID
		ELSE SUBLIS(W, '(EQUIVALENT PPP QQQ));
	(INST(WFF1 CONS WFF2, '((IMPLIES PPP QQQ) IMPLIES QQQ PPP), NIL));


EXPR ERREND (MESSAGE);
	BEGIN
	PRINT MESSAGE;
	ERR();
	END;


EXPR FREEIN (VAR, LINES);
	IF NULL LINES THEN NIL
	ELSE IF VAR ε FREEVARS(WFFPART(CAR LINES)) THEN T
	ELSE FREEIN(VAR, CDR LINES);


EXPR FREEVARS (EXPRESSION);
	FREEVARS1(NIL, NIL, EXPRESSION);


EXPR FREEVARS1 (BVARS, FVARS, EXP);
	IF ATOM EXP THEN 
		IF ISVAR(EXP) THEN 
			IF EXP ε BVARS THEN FVARS
			ELSE IF EXP ε FVARS THEN FVARS
			ELSE EXP CONS FVARS
		ELSE FVARS
	ELSE IF ATOM CAR EXP THEN FREEVARS2(BVARS, FVARS, CDR EXP)
	ELSE IF ATOM EXP[1,1] THEN 
		(IF EXP[1,1] ε '(FORALL THEREEXISTS) THEN 
			FREEVARS1(EXP[1,2] CONS BVARS, FVARS, EXP[3]))
	ELSE ERREND('(UNKNOWN NONATOMIC FUNCTION));


EXPR FREEVARS2 (BVARS, FVARS, EXPL);
	IF NULL EXPL THEN FVARS
	ELSE FREEVARS1(BVARS, FREEVARS2(BVARS, FVARS, CDR EXPL), CAR EXPL);


EXPR GETCURLINE ();
	GETLINE(CURLINE());


EXPR GETLINE (LINENO);
	BEGIN
	NEW TEM;
	TEM ← ASSOC(LINENO, CURTEXT());
	IF NULL TEM THEN ERREND('(NO SUCH LINE));
	RETURN TEM;
	END;


FEXPR GIVEPROOF (L);
	BEGIN
	IF ¬ATOM CAR L THEN ERREND('(NON ATOMIC PROOF NAME));
	IF ¬(CAR L ε PROOFS) THEN PROOFS ← PROOFS @ <CAR L>;
	PUTPROP(CAR L, L[2], 'PROOF);
	END;


EXPR IFE1 (WFF1, WFF2);
	LAMBDA (W, X, Y, Z); 
		IF VALID(W) THEN SUBLIS(W, 'QQQ)
		ELSE IF VALID(X) THEN SUBLIS(X, 'RRR)
		ELSE IF VALID(Y) THEN SUBLIS(Y, 'QQQ)
		ELSE IF VALID(Z) THEN SUBLIS(Z, 'RRR)
		ELSE 'INVALID;
	(INST(WFF1 CONS WFF2, '(PPP COND (PPP QQQ) (T RRR)), NIL), INST(WFF1 CONS WFF2, '((NOT PPP) COND (PPP 
		QQQ) (T RRR)), NIL), INST(WFF2 CONS WFF1, '(PPP COND (PPP QQQ) (T RRR)), NIL), INST(WFF2 CONS 
		WFF1, '((NOT PPP) COND (PPP QQQ) (T RRR)), NIL));


EXPR IFI1 (WFF1, WFF2);
	LAMBDA (W, X); 
		IF VALID(W) THEN SUBLIS(W, '(COND (PPP QQQ) (T RRR)))
		ELSE IF VALID(X) THEN SUBLIS(X, '(COND (PPP QQQ) (T RRR)))
		ELSE 'INVALID;
	(INST(WFF1 CONS WFF2, '((IMPLIES PPP QQQ) IMPLIES (NOT PPP) RRR), NIL), INST(WFF2 CONS WFF1, '((IMPLIES
		 PPP QQQ) IMPLIES (NOT PPP) RRR), NIL));


EXPR INITALL ();
	BEGIN
	CURPRF ← NIL;
	AXIOMS ← NIL;
	THEOREMS ← NIL;
	PROOFS ← NIL;
	SCHEMAS ← NIL;
	END;


EXPR INITOPS ();
	BEGIN
	NEW INCR, OP, PREC, PRECLIS;
	PRECLIS ← '?*COMMA?* CONS 'SETQ CONS PRECLIS?*;
LOOP; 	IF NULL PRECLIS THEN RETURN NIL;
	OP ← CAR PRECLIS;
	PREC ← GET(OP, 'INFIX);
	INCR ← 	IF GET(OP, 'LEFT) THEN MINUS 1
		ELSE 1;
	PUTPROP(OP, <3 * PREC + INCR, 3 * PREC - INCR>, 'PREC);
	PRECLIS ← CDR PRECLIS;
	GO LOOP;
	END;


EXPR INITPROOF (NAME);
	BEGIN
	IF NULL NAME THEN ERREND('(NIL NOT ACCEPTABLE PROOF NAME));
	CURPRF ← NAME;
	IF GETL(NAME, '(PROOF)) THEN GO EXIST;
	PUTPROP(NAME, NIL, 'PROOF);
	PROOFS ← PROOFS @ <NAME>;
EXIST; 	CURLIN ← 
		IF NULL CURTEXT() THEN 0
		ELSE (LAST CURTEXT())[1,1];
	PUTPROP('?@, CURLINE(), 'NEWNAM);
	END;


EXPR INITSTANCHARSET ();
	BEGIN
	PUTPROP('AND, '?∧, 'INFXNAM);
	PUTPROP('CMAPS, '?→?→, 'INFXNAM);
	PUTPROP('?*COMMA?*, '?,, 'INFXNAM);
	PUTPROP('CONS, '?., 'INFXNAM);
	PUTPROP('CONTAINED, '?⊂, 'INFXNAM);
	PUTPROP('DIFFERENCE, '?-, 'INFXNAM);
	PUTPROP('EQUAL, '?=, 'INFXNAM);
	PUTPROP('EQUIVALENT, '?≡, 'INFXNAM);
	PUTPROP('EXPT, '?↑, 'INFXNAM);
	PUTPROP('FORALL, '?∀, 'INFXNAM);
	PUTPROP('GEQ, '?≥, 'INFXNAM);
	PUTPROP('GREATERP, '?>, 'INFXNAM);
	PUTPROP('IMPLIES, '?⊃, 'INFXNAM);
	PUTPROP('INTERSECTION, '?∩, 'INFXNAM);
	PUTPROP('LAMBDA, '?λ, 'INFXNAM);
	PUTPROP('LEQ, '?≤, 'INFXNAM);
	PUTPROP('LESSP, '?<, 'INFXNAM);
	PUTPROP('MAPS, '?→, 'INFXNAM);
	PUTPROP('MEMBER, '?ε, 'INFXNAM);
	PUTPROP('MINUS, '?-, 'INFXNAM);
	PUTPROP('NEQ, '?≠, 'INFXNAM);
	PUTPROP('NOT, '?¬, 'INFXNAM);
	PUTPROP('OR, '?∨, 'INFXNAM);
	PUTPROP('PLUS, '?+, 'INFXNAM);
	PUTPROP('PRODUCT, '?⊗, 'INFXNAM);
	PUTPROP('QUOTE, '?', 'INFXNAM);
	PUTPROP('QUOTIENT, '?/, 'INFXNAM);
	PUTPROP('SETQ, '?←, 'INFXNAM);
	PUTPROP('THEREEXISTS, '?∃, 'INFXNAM);
	PUTPROP('TIMES, '?*, 'INFXNAM);
	PUTPROP('UNION, '?∪, 'INFXNAM);
	END;


EXPR INITTTYCHARSET ();
	BEGIN
	PUTPROP('AND, '?&, 'INFXNAM);
	PUTPROP('CMAPS, '? CMAPS? , 'INFXNAM);
	PUTPROP('?*COMMA?*, '?,, 'INFXNAM);
	PUTPROP('CONS, '?., 'INFXNAM);
	PUTPROP('CONTAINED, '? CONT? , 'INFXNAM);
	PUTPROP('DIFFERENCE, '?-, 'INFXNAM);
	PUTPROP('EQUAL, '?=, 'INFXNAM);
	PUTPROP('EQUIVALENT, '?<?=?>, 'INFXNAM);
	PUTPROP('EXPT, '?↑, 'INFXNAM);
	PUTPROP('FORALL, 'A, 'INFXNAM);
	PUTPROP('GEQ, '?>?=, 'INFXNAM);
	PUTPROP('GREATERP, '?>, 'INFXNAM);
	PUTPROP('IMPLIES, '?=?>, 'INFXNAM);
	PUTPROP('INTERSECTION, '? INTERSECT? , 'INFXNAM);
	PUTPROP('LAMBDA, 'L, 'INFXNAM);
	PUTPROP('LEQ, '?<?=, 'INFXNAM);
	PUTPROP('LESSP, '?<, 'INFXNAM);
	PUTPROP('MAPS, '? MAPS? , 'INFXNAM);
	PUTPROP('MEMBER, '? MEMBER? , 'INFXNAM);
	PUTPROP('MINUS, '?-, 'INFXNAM);
	PUTPROP('NEQ, '? NEQ? , 'INFXNAM);
	PUTPROP('NOT, '?-, 'INFXNAM);
	PUTPROP('OR, '? V? , 'INFXNAM);
	PUTPROP('PLUS, '?+, 'INFXNAM);
	PUTPROP('PRODUCT, '? PROD? , 'INFXNAM);
	PUTPROP('QUOTE, '?', 'INFXNAM);
	PUTPROP('QUOTIENT, '?/, 'INFXNAM);
	PUTPROP('SETQ, '?←, 'INFXNAM);
	PUTPROP('THEREEXISTS, 'E, 'INFXNAM);
	PUTPROP('TIMES, '?*, 'INFXNAM);
	PUTPROP('UNION, '? UNION? , 'INFXNAM);
	END;


EXPR INST (EXP, MODEL, PAIRS);
	IF ¬VALID(PAIRS) THEN 'INVALID
	ELSE IF ATOM MODEL THEN 
		IF MODEL ε '(PPP QQQ RRR SSS) THEN 
			LAMBDA (W); 
				IF NULL W THEN (MODEL CONS EXP) CONS PAIRS
				ELSE IF CDR W = EXP THEN PAIRS
				ELSE 'INVALID;
			(ASSOC(MODEL, PAIRS))
		ELSE IF MODEL EQ EXP THEN PAIRS
		ELSE 'INVALID
	ELSE IF ATOM EXP THEN 'INVALID
	ELSE INST(CDR EXP, CDR MODEL, INST(CAR EXP, CAR MODEL, PAIRS));


EXPR ISCONST (X);
	NUMBERP X | X ε LOGICALCONSTANTS;


EXPR ISEQUIVALENCE (WFF);
	WFF ε '(EQUAL EQUIVALENT SETQ);


EXPR ISIDENT (X);
	ATOM X & ¬NUMBERP X;


EXPR ISQUANT (X);
	X ε QUANTIFIERS;


EXPR ISVAR (X);
	ISIDENT(X) & ¬ISCONST(X);


EXPR LAMEXP (FORMULA);
	IF ATOM FORMULA THEN FORMULA
	ELSE IF ATOM CAR FORMULA THEN CAR FORMULA CONS LAMEXPL(CDR FORMULA)
	ELSE IF FORMULA[1,1,1] = 'LAMBDA THEN PROPSUBST(FORMULA[2], FORMULA[1,1,2], FORMULA[1,2])
	ELSE LAMEXP(CAR FORMULA) CONS LAMEXPL(CDR FORMULA);


EXPR LAMEXPL (LIST);
	MAPCAR(FUNCTION(LAMEXP), LIST);


EXPR MAKECONSES (L);
	BEGIN
	NEW RES;
LOOP; 	IF NULL L THEN RETURN RES;
	IF ATOM CAR L | L[1,1] NEQ 'CONS | LENGTH CAR L NEQ 3 THEN ERREND('(BAD ARGUMENT));
	RES ← (L[1,2] CONS L[1,3]) CONS RES;
	L ← CDR L;
	GO LOOP;
	END;


EXPR MAKERNL (FREEV, ALLV);
	BEGIN
	NEW CNT, ID, NVAR, NEWVARS, VAR;
LOOP; 	IF NULL FREEV THEN RETURN NEWVARS;
	VAR ← CAR FREEV;
	IF VAR ε ALLV THEN GO MAKE;
ELOOP; 	FREEV ← CDR FREEV;
	GO LOOP;
MAKE; 	ID ← ALPHAPART(VAR);
	CNT ← 1;
MAKE1; 	NVAR ← MAKESYM(ID, CNT);
	IF NVAR ε ALLV THEN GO EMAKE;
	NEWVARS ← (VAR CONS NVAR) CONS NEWVARS;
	GO ELOOP;
EMAKE; 	CNT ← CNT + 1;
	GO MAKE1;
	END;


EXPR MAKEVAR (V, L);
	BEGIN
	NEW TEM;
	TEM ← MAKERNL(<V>, L);
	RETURN (IF NULL TEM THEN V
		ELSE CDAR TEM);
	END;


EXPR MAKESYM (IDENT, NUM);
	READLIST (EXPLODE IDENT @ EXPLODE NUM);


EXPR MAKETHEOREM1 (THEOREM, LINE, PROOF);
	BEGIN
	INITPROOF(PROOF);
	IF ¬NULL ASSPART(LINE) THEN ERREND('(STILL HAS ASSUMPTIONS));
	PUTPROP(THEOREM, WFFPART(LINE), 'THEOREM);
	PUTPROP(THEOREM, <LINE, PROOF>, 'BY);
	THEOREMS ← THEOREMS @ <THEOREM>;
	IF ?*PRINT THEN SHOWTHEOREM(THEOREM);
	END;


EXPR MP1 (U, V);
	BEGIN
	NEW W;
	W ← INST(U CONS V, '(PPP IMPLIES PPP QQQ), NIL);
	IF ¬VALID(W) THEN W ← INST(V CONS U, '(PPP IMPLIES PPP QQQ), NIL);
	IF ¬VALID(W) THEN RETURN 'INVALID
	ELSE RETURN SUBLIS(W, 'QQQ);
	END;


EXPR NEXTLINE ();
	CURLINE() + 1;


EXPR NOTELIM (X, NOTX);
	LAMBDA (X, Y); 
		IF ¬VALID(X) THEN Y
		ELSE X;
	(INST(X CONS NOTX, '(PPP NOT PPP), NIL), INST(NOTX CONS X, '(PPP NOT PPP), NIL));


EXPR NOTINTRO (PROP);
	LAMBDA (W); 
		IF ¬VALID(W) THEN 'INVALID
		ELSE SUBLIS(W, '(NOT PPP));
	(INST(PROP, '(IMPLIES PPP FALSE), NIL));


EXPR NTHCDR (L, N);
	IF N = 0 THEN L
	ELSE NTHCDR(CDR L, N - 1);


EXPR NTHELT (L, N);
	CAR NTHCDR(L, N - 1);


EXPR NUMPART (LINE);
	CAR GETLINE(LINE);


EXPR ORELIM1 (DISJUN, IMPS);
	BEGIN
	NEW ANTECEDS, PREMS, RES;
	IF CAR DISJUN NEQ 'OR THEN ERREND('(FIRST ARG MUST BE DISJUNCTION));
	IF NULL CDR DISJUN THEN ERREND('(NO DISJUNCTS));
	IF NULL IMPS THEN ERREND('(NEED AT LEAST ONE IMPLICATION));
	PREMS ← CDR DISJUN;
	RES ← CDDAR IMPS;
LOOP1; 	IF IMPS[1,1] NEQ 'IMPLIES THEN ERREND('(ARG NOT IMPLICATION));
	IF CDDAR IMPS NEQ RES THEN ERREND('(MULTIPLE CONCLUSIONS));
	ANTECEDS ← IMPS[1,2] CONS ANTECEDS;
	IF ¬NULL (IMPS ← CDR IMPS) THEN GO LOOP1;
LOOP2; 	IF NULL PREMS THEN RETURN CAR RES;
	IF ¬(CAR PREMS ε ANTECEDS) THEN ERREND('(UNPROVEN DISJUNCT));
	PREMS ← CDR PREMS;
	GO LOOP2;
	END;


EXPR PCERR ();
	BEGIN
	PRINT 'PROOF?-CHECKER;
	LINELENGTH CONSOLEWIDTH;
	BEGIN
	?*FILEPRINT ← NIL;
	END;
	BEGIN
	?*PRINT ← T;
	END;
	BEGIN
	?*TWODIM ← NIL;
	END;
	EVAL '(BEGIN);
	END;


EXPR PCINIT ();
	BEGIN
	EXCISE();
	ONDD();
	INITOPS();
	INITALL();
	INITFN 'PCSTART;
	PRINT 'PROOF? CHECKER? INITIALIZED;
	END;


EXPR PCSTART ();
	BEGIN
	EVAL '(ERRSET (RESTOREALL (CONS PCHECK INI)) NIL);
	INITFN 'PCERR;
	PCERR();
	END;


EXPR PAIRLIS (CARS, CDRS);
	IF NULL CARS | NULL CDRS THEN NIL
	ELSE (CAR CARS CONS CAR CDRS) CONS PAIRLIS(CDR CARS, CDR CDRS);


EXPR QUANTEQUIV (EXP1, CONT1, EXP2, CONT2);
	BEGIN
	NEW GEN, TEM;
	IF ATOM EXP1 THEN GO ATOM
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  ATOM
                                 ;
	IF ATOM CAR EXP1 THEN GO FUN;
	IF ISQUANT(EXP1[1,1]) THEN GO QUANT;
LIST; 	IF NULL EXP1 THEN RETURN NULL EXP2;
	IF ¬QUANTEQUIV(CAR EXP1, CONT1, CAR EXP2, CONT2) THEN RETURN NIL;
	EXP1 ← CDR EXP1;
	EXP2 ← CDR EXP2;
	GO LIST;
ATOM
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  ATOM
    ; 	TEM ← ASSOC(EXP1, CONT1);
	IF ¬NULL TEM THEN EXP1 ← CDAR TEM;
	TEM ← ASSOC(EXP2, CONT2);
	IF ¬NULL TEM THEN EXP1 ← CDAR TEM;
	RETURN (EXP1 = EXP2);
FUN; 	IF CAR EXP1 NEQ CAR EXP2 THEN RETURN NIL;
	EXP1 ← CDR EXP1;
	EXP2 ← CDR EXP2;
	GO LIST;
QUANT; 	IF ¬ISQUANT(EXP2[1,1]) | EXP1[1,1] NEQ EXP2[1,1] THEN RETURN NIL;
	GEN ← GENSYM();
	RETURN QUANTEQUIV(EXP1[2], (EXP1[1,2] CONS GEN) CONS CONT1, EXP2[2], (EXP2[1,2] CONS GEN) CONS CONT2)
		;
	END;


EXPR PROPSUBST (TERM, VAR, EXP);
	PROPSUBST1(TERM, VAR, EXP, MAKERNL(FREEVARS(TERM), ALLVARS(EXP)));


EXPR PROPSUBST1 (TERM, VAR, EXP, RNL);
	IF ATOM EXP THEN 
		IF ISVAR(EXP) THEN 
			IF EXP = VAR THEN TERM
			ELSE EXP
		ELSE EXP
	ELSE IF ¬ATOM CAR EXP & ISQUANT(EXP[1,1]) THEN 
		BEGIN
		NEW NEWNAM;
		NEWNAM ← ASSOC(EXP[1,2], RNL);
		NEWNAM ← 
			IF NULL NEWNAM THEN EXP[1,2]
			ELSE CDR NEWNAM;
		RETURN <<EXP[1,1], NEWNAM>, PROPSUBST1(TERM, VAR, SUBST(NEWNAM, EXP[1,2], EXP[2]), RNL)>;
		END
	ELSE PROPSUBST1(TERM, VAR, CAR EXP, RNL) CONS PROPSUBSTL(TERM, VAR, CDR EXP, RNL);


EXPR PROPSUBSTL (TERM, VAR, EXPL, RNL);
	IF NULL EXPL THEN NIL
	ELSE PROPSUBST1(TERM, VAR, CAR EXPL, RNL) CONS PROPSUBSTL(TERM, VAR, CDR EXPL, RNL);


EXPR REPEITHER (WFF, EQUAT, FLAG, ORD);
	IF ¬ISEQUIVALENCE(CAR EQUAT) THEN ERREND('(NO EQUATION))
	ELSE REPNTH(
		IF FLAG THEN EQUAT[3]
		ELSE EQUAT[2], 
		IF FLAG THEN EQUAT[2]
		ELSE EQUAT[3], WFF, ORD);


EXPR REPNTH (NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                , OLD, EXP, NUM);
	BEGIN
	NEW NEWEXP, ORDCNT;
	ORDCNT ← 0;
	NEWEXP ← REPNTH1(NEW
*** WARNING, MLISP RESERVED WORD:  NEW
                            , OLD, EXP, NIL, NUM);
	IF ORDCNT ?*LESS NUM THEN ERREND('(NO REPLACEMENT));
	RETURN NEWEXP;
	END;


EXPR REPNTH1 (NEXP, OEXP, EXP, CON, NUM);
	BEGIN
	NEW BVAR, GEN, NVAR;
	IF QUANTEQUIV(OEXP, NIL, EXP, CON) THEN GO GOTIT;
	IF ATOM EXP THEN RETURN EXP;
	IF ATOM CAR EXP THEN RETURN (CAR EXP CONS REPNTHL(NEXP, OEXP, CDR EXP, CON, NUM));
	IF ISQUANT(EXP[1,1]) THEN GO QUANT;
QUANT; 	GEN ← GENSYM();
	BVAR ← EXP[1,2];
	NVAR ← 	IF BVAR ε ALLVARS(NEXP) THEN MAKEVAR(BVAR, ALLVARS(EXP[2]))
		ELSE BVAR;
	RETURN <<EXP[1,1], NVAR>, REPNTH1(NEXP, OEXP, SUBST(NVAR, BVAR, EXP[2]), (NVAR CONS GEN) CONS CON, NUM
		)>;
GOTIT; 	ORDCNT ← ORDCNT + 1;
	RETURN (IF ORDCNT = NUM THEN NEXP
		ELSE EXP);
	END;


EXPR REPNTHL (NEXP, OEXP, LST, CON, NUM);
	IF NULL LST THEN NIL
	ELSE REPNTH1(NEXP, OEXP, CAR LST, CON, NUM) CONS REPNTHL(NEXP, OEXP, CDR LST, CON, NUM);


EXPR SAVEAXIOM (AXIOM);
	PRINTEXPR(<'ADDAXIOM, AXIOM, GET(AXIOM, 'AXIOM)>);


EXPR SAVEAXCOM (AXIOM);
	PRINTEXPR(<'GIVEAX, AXIOM, GET(AXIOM, 'AXIOM)>);


EXPR SAVEPRFCOM (PROOF);
	BEGIN
	NEW PRF;
	PRINT <'PROOF, PROOF>;
	PRF ← GET(PROOF, 'PROOF);
LOOP; 	IF NULL PRF THEN RETURN TERPRI();
	IF PRF[1,3,1] = 'USETHM THEN SAVETHMCOM(PRF[1,3,2]);
	PRINT PRF[1,1];
	PRINC '?	;
	PRINTSUBEXPR(PRF[1,3], 9, 0);
	PRF ← CDR PRF;
	GO LOOP;
	END;


EXPR SAVEPROOF (PROOF);
	PRINTEXPR(<'GIVEPROOF, PROOF, GET(PROOF, 'PROOF)>);


EXPR SAVESCHEMA (SCHEMA);
	PRINTEXPR(<'ADDSCHEMA, SCHEMA, GET(SCHEMA, 'SCHEMA)>);


EXPR SAVESCHMCOM (SCHEMA);
	PRINTEXPR(<'GIVESCHM, SCHEMA, GET(SCHEMA, 'SCHEMA)>);


EXPR SAVETHEOREM (THEOREM);
	PRINTEXPR(<'ADDTHM, THEOREM, CAR GET(THEOREM, 'BY), GET(THEOREM, 'BY)[2]>);


EXPR SAVETHMCOM (THEOREM);
	PRINTEXPR(<'MAKETHM, THEOREM, CAR GET(THEOREM, 'BY), GET(THEOREM, 'BY)[2]>);


EXPR SETDIF (X, Y);
	BEGIN
	NEW ANS;
LOOP; 	IF NULL X THEN RETURN REVERSE ANS;
	IF ¬(CAR X ε Y) THEN ANS ← CAR X CONS ANS;
	X ← CDR X;
	GO LOOP;
	END;


EXPR SHOWAXIOM (NAME);
	BEGIN
	PRINT 'AXIOM;
	PRINC NAME;
	TERPRI();
	SHOWEXP(GET(NAME, 'AXIOM));
	TERPRI();
	END;


EXPR SHOWCURLINE ();
	IF CURLINE() = 0 THEN SHOW()
	ELSE SHOWLINE(GETCURLINE());


EXPR SHOWEXP (EXP);
	IF ?*TWODIM THEN TDDEXP(EXP, CURCOL(), 0)
	ELSE INFX(EXP);


EXPR SHOWLINE (LINTXT);
	BEGIN
	NEW COM;
	TERPRI();
	TERPRI();
	PRINC CAR LINTXT;
	PRINC ':;
	PRINC '?	;
	SHOWEXP(LINTXT[2]);
	PRINS('BY);
	COM ← LINTXT[3];
	IF CAR COM = 'ASS THEN GO ASS;
	IF CAR COM = 'USEAX THEN COM ← 'AXIOM CONS CDR COM;
	IF CAR COM = 'USESCHM THEN COM ← 'SCHEMA CONS CDR COM;
	IF CAR COM = 'USETHM THEN COM ← 'THEOREM CONS CDR COM;
	SHOWEXP(COM);
	IF NULL LINTXT[4] THEN RETURN NIL;
	PRINS('ASSUMING);
	PRINS(LINTXT[4]);
	RETURN NIL;
ASS; 	PRINS('ASSUMPTION);
	END;


EXPR SHOWPROOF (NAME);
	BEGIN
	PRINT 'PROOF;
	PRINS(NAME);
	MAPC(FUNCTION(SHOWLINE), GET(NAME, 'PROOF));
	TERPRI();
	END;


EXPR SHOWSCHEMA (NAME);
	BEGIN
	PRINT 'SCHEMA;
	PRINC NAME;
	TERPRI();
	SHOWEXP(GET(NAME, 'SCHEMA));
	TERPRI();
	END;


EXPR SHOWTHEOREM (NAME);
	BEGIN
	PRINT 'THEOREM;
	PRINS(NAME);
	TERPRI();
	SHOWEXP(GET(NAME, 'THEOREM));
	END;


EVAL '(DEFPROP AXIOM SHOWAXIOM IMAGE);


EVAL '(DEFPROP PROOF SHOWPROOF IMAGE);


EVAL '(DEFPROP SCHEMA SHOWSCHEMA IMAGE);


EVAL '(DEFPROP THEOREM SHOWTHEOREM IMAGE);


EXPR SPECALL (FORM, ARGS);
	BEGIN
LOOP; 	IF NULL ARGS THEN RETURN FORM;
	IF ATOM FORM THEN ERREND('(ATOMIC EXPRESSION));
	IF FORM[1,1] NEQ 'FORALL & FORM[1,1] NEQ 'THEREEXISTS THEN ERREND('(NOT QUANTIFIED EXPRESSION));
	RETURN SPECALL(PROPSUBST(CAR ARGS, FORM[1,2], FORM[2]), CDR ARGS);
	END;


EXPR TH1 (A1, A2, A, C);
	IF NULL A THEN TH2(A1, A2, NIL, NIL, C)
	ELSE CAR A ε C | (
		IF ATOM CAR A THEN TH1(
			IF CAR A ε A1 THEN A1
			ELSE CAR A CONS A1, A2, CDR A, C)
		ELSE TH1(A1, 
			IF CAR A ε A2 THEN A2
			ELSE CAR A CONS A2, CDR A, C));


EXPR TH2 (A1, A2, C1, C2, C);
	IF NULL C THEN TH(A1, A2, C1, C2)
	ELSE IF ATOM CAR C THEN TH2(A1, A2, 
		IF CAR C ε C1 THEN C1
		ELSE CAR C CONS C1, C2, CDR C)
	ELSE TH2(A1, A2, C1, 
		IF CAR C ε C2 THEN C2
		ELSE CAR C CONS C2, CDR C);


EXPR TH (A1, A2, C1, C2);
	IF NULL A2 THEN ¬NULL C2 & THR(CAR C2, A1, A2, C1, CDR C2)
	ELSE THL(CAR A2, A1, CDR A2, C1, C2);


EXPR THL (U, A1, A2, C1, C2);
	IF CAR U = 'NOT THEN TH1R(U[2], A1, A2, C1, C2)
	ELSE IF CAR U = 'AND THEN TH2L(CDR BINAND(CDR U), A1, A2, C1, C2)
	ELSE IF CAR U = 'OR THEN 
		TH1L(BINOR(CDR U)[2], A1, A2, C1, C2) & TH1L(BINOR(CDR U)[3], A1, A2, C1, C2)
	ELSE IF CAR U = 'IMPLIES THEN TH1L(U[3], A1, A2, C1, C2) & TH1R(U[2], A1, A2, C1, C2)
	ELSE IF CAR U = 'EQUIVALENT THEN TH2L(CDR U, A1, A2, C1, C2) & TH2R(CDR U, A1, A2, C1, C2)
	ELSE IF U ε C1 THEN T
	ELSE TH(U CONS A1, A2, C1, C2);


EXPR THR (U, A1, A2, C1, C2);
	IF CAR U = 'NOT THEN TH1L(U[2], A1, A2, C1, C2)
	ELSE IF CAR U = 'AND THEN TH1R(U[2], A1, A2, C1, C2) & TH1R(U[3], A1, A2, C1, C2)
	ELSE IF CAR U = 'OR THEN TH2R(CDR U, A1, A2, C1, C2)
	ELSE IF CAR U = 'IMPLIES THEN TH11(CDR U, A1, A2, C1, C2)
	ELSE IF CAR U = 'EQUIVALENT THEN TH11(CDR U, A1, A2, C1, C2) & TH11(REVERSE CDR U, A1, A2, C1, C2)
	ELSE IF U ε A1 THEN T
	ELSE TH(A1, A2, U CONS C1, C2);


EXPR TH1L (V, A1, A2, C1, C2);
	IF ATOM V THEN V ε C1 | TH(V CONS A1, A2, C1, C2)
	ELSE V ε C2 | TH(A1, V CONS A2, C1, C2);


EXPR TH1R (V, A1, A2, C1, C2);
	IF ATOM V THEN V ε A1 | TH(A1, A2, V CONS C1, C2)
	ELSE V ε A2 | TH(A1, A2, C1, V CONS C2);


EXPR TH2L (V, A1, A2, C1, C2);
	IF ATOM CAR V THEN CAR V ε C1 | TH1L(V[2], CAR V CONS A1, A2, C1, C2)
	ELSE CAR V ε C2 | TH1L(V[2], A1, CAR V CONS A2, C1, C2);


EXPR TH2R (V, A1, A2, C1, C2);
	IF ATOM CAR V THEN CAR V ε A1 | TH1R(V[2], A1, A2, CAR V CONS C1, C2)
	ELSE CAR V ε A2 | TH1R(V[2], A1, A2, C1, CAR V CONS C2);


EXPR TH11 (V, A1, A2, C1, C2);
	IF ATOM CAR V THEN CAR V ε C1 | TH1R(V[2], CAR V CONS A1, A2, C1, C2)
	ELSE CAR V ε C2 | TH1R(V[2], A1, CAR V CONS A2, C1, C2);


EXPR UNGEN (WFF, ASS, FVAR, BVAR);
	BEGIN
	NEW TEM;
	IF FREEIN(FVAR, ASS) THEN ERREND('(VARIABLE FREE IN ASSUMPTIONS));
	IF USEDINEXISTSPEC(FVAR) THEN ERREND('(USED IN EXISTENTIALLY SPECIFIED LINE));
	TEM ← GENSYM();
	WFF ← SUBST(TEM, FVAR, WFF);
	IF BVAR ε ALLVARS(WFF) THEN ERREND('(VARIABLE CONFLICT));
	RETURN <<'FORALL, BVAR>, SUBST(BVAR, TEM, WFF)>;
	END;


EXPR UNION (SETS);
	IF NULL SETS THEN NIL
	ELSE IF NULL CDR SETS THEN CAR SETS
	ELSE UNION2(CAR SETS, UNION(CDR SETS));


EXPR UNION2 (SET1, SET2);
	IF NULL SET1 THEN SET2
	ELSE IF CAR SET1 ε SET2 THEN UNION2(CDR SET1, SET2)
	ELSE UNION2(CDR SET1, CAR SET1 CONS SET2);


EXPR USEDINEXISTSPEC (VAR);
	BEGIN
	NEW PRF;
	PRF ← CURTEXT();
LOOP; 	IF NULL PRF THEN RETURN NIL;
	IF PRF[1,3,1] = 'ES & VAR ε FREEVARS(PRF[1,2]) THEN RETURN T;
	PRF ← CDR PRF;
	GO LOOP;
	END;


EXPR USEDVAR (VAR);
	BEGIN
	NEW PRF;
	PRF ← CURTEXT();
LOOP; 	IF NULL PRF THEN RETURN NIL;
	IF VAR ε ALLVARS(PRF[1,2]) THEN RETURN T;
	PRF ← CDR PRF;
	GO LOOP;
	END;


EXPR VALID (PROP);
	PROP NEQ 'INVALID;


EXPR WFFLIST (L);
	MAPCAR(FUNCTION(WFFPART), L);


EXPR WFFPART (LINE);
	GETLINE(LINE)[2];


EXPR GETINFXNAM (ATOM
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  ATOM
                     );
	BEGIN
	NEW NAME;
	IF NUMBERP ATOM
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  ATOM
                        THEN RETURN ATOM
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  ATOM
                                        ;
	NAME ← SEEKPROP(ATOM
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  ATOM
                            , 'INFXNAM);
	IF ¬NULL NAME THEN RETURN NAME[2];
	RETURN ATOM
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  ATOM
                   ;
	END;


EXPR INFX (EXP);
	BEGIN
	INFXEXPR(EXP, 0, 0);
	INFXATOM('? );
	END;


EXPR INFXARGS (ARGS, LPREC, RPREC);
	IF NULL ARGS THEN 
		BEGIN
		INFXATOM('?();
		INFXATOM('?));
		END
	ELSE IF NULL CDR ARGS THEN 
		BEGIN
		INFXATOM('? );
		INFXEXPR(CAR ARGS, LPREC, RPREC);
		END
	ELSE INFXPARENED('?*COMMA?* CONS ARGS, LPREC, RPREC);


PUTPROP('INFXATOM, 'PRNTATOM, 'EXPR);


EXPR INFXCOND (S, L, R);
	BEGIN
	INFXATOM('IF);
	INFXATOM('? );
	INFXEXPR(S[2,1], 0, 0);
	INFXATOM('? );
	INFXATOM('THEN);
	INFXATOM('? );
	INFXEXPR(S[2,2], 0, 0);
	INFXATOM('? );
	IF NULL CDDR S THEN RETURN NIL;
	INFXATOM('ELSE);
	INFXATOM('? );
	INFXEXPR(S[3,2], 0, 0);
	END;


EXPR INFXFUN (FN, LPREC, RPREC);
	IF ATOM FN THEN INFXATOM(FN)
	ELSE INFXPARENED(FN, LPREC, RPREC);


EXPR INFXEXPR (EXP, LPREC, RPREC);
	BEGIN
	NEW OP;
	IF ATOM EXP THEN RETURN INFXATOM(EXP);
	IF ¬ATOM CAR EXP THEN GO NOATM;
	OP ← GETGET(CAR EXP, 'INFXFUN);
	IF ¬NULL OP THEN RETURN APPLY(OP[2], <EXP, LPREC, RPREC>);
NOATM; 	INFXFUN(CAR EXP, LPREC, RPREC);
	INFXARGS(CDR EXP, 10000, RPREC);
	END;


EXPR INFXLIST (OP, ARGS, LPREC, RPREC);
	BEGIN
	NEW PREC;
	PREC ← GET(OP, 'PREC);
LOOP; 	IF NULL ARGS THEN RETURN NIL;
	INFXATOM(OP);
	INFXEXPR(CAR ARGS, PREC[2], 
		IF NULL CDR ARGS THEN RPREC
		ELSE CAR PREC);
	ARGS ← CDR ARGS;
	GO LOOP;
	END;


EXPR INFXOPER (EXP, LPREC, RPREC);
	BEGIN
	NEW PREC;
	PREC ← GET(CAR EXP, 'PREC);
	IF CAR PREC ?*LESS LPREC | PREC[2] ?*LESS RPREC THEN RETURN INFXPARENED(EXP, LPREC, RPREC);
	IF NULL CDR EXP THEN RETURN INFXATOM(CAR EXP);
	IF NULL CDDR EXP THEN RETURN INFXLIST(CAR EXP, CDR EXP, LPREC, RPREC);
	INFXEXPR(EXP[2], LPREC, CAR PREC);
	RETURN INFXLIST(CAR EXP, CDDR EXP, LPREC, RPREC);
	END;


EXPR INFXPARENED (EXP, LPREC, RPREC);
	BEGIN
	INFXATOM('?();
	INFXEXPR(EXP, 0, 0);
	INFXATOM('?));
	END;


EXPR INFXQUOTE (SEXPR, LPREC, RPREC);
	BEGIN
	INFXATOM('QUOTE);
	PRIN1 SEXPR[2];
	END;


EXPR INFXSPEC (SEXPR, LPREC, RPREC);
	LAMBDA (G0016); 
		G0016(SEXPR, LPREC, RPREC);
	(GET(CAR SEXPR, 'SPECOPER));


EXPR PRNTATOM (AT
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  AT
                 );
	BEGIN
	NEW NAM;
	NAM ← GETINFXNAM(AT
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  AT
                           );
	IF CHRCT() ?*LESS FLATSIZE NAM + 1 THEN TERPRI();
	PRINC NAM;
	END;


PUTPROP('PREC, 'INFXOPER, 'INFXFUN);


PUTPROP('SPECOPER, 'INFXSPEC, 'INFXFUN);


PUTPROP('COND, 'INFXCOND, 'SPECOPER);


PUTPROP('QUOTE, 'INFXQUOTE, 'SPECOPER);


EXPR FITSLINE (EXP, COL, PARS);
	BEGIN
	NEW ANS, EXPEXP, EXPLGTH, EXPLIM;
	IF ATOM EXP THEN RETURN T;
	EXPLGTH ← 0;
	EXPEXP ← EXP;
	EXPLIM ← LINELENGTH NIL - (COL + PARS);
	INITPROP('INFXATOM, 'LGTHATOM, 'EXPR);
	ANS ← EVAL '(ERRSET (INFXEXPR EXPEXP 1 0));
	DELETEPROP('INFXATOM, 'EXPR);
	RETURN ANS;
	END;


EXPR LGTHATOM (AT
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  AT
                 );
	BEGIN
	EXPLGTH ← EXPLGTH + FLATSIZE GETINFXNAM(AT
*** WARNING, MLISP PREFIX NOT USED AS A PREFIX:  AT
                                                  );
	IF LEQ(EXPLGTH, EXPLIM) THEN RETURN NIL;
	EXPLGTH ← NIL;
	ERR();
	END;


EXPR TDD (EXP);
	TDDEXP(EXP, 1, 0);


EXPR TDDARGS (ARGS, COL, PARS);
	IF ¬NULL ARGS & NULL CDR ARGS THEN 
		BEGIN
		PRINC '? ;
		TDDEXP(CAR ARGS, COL + 1, PARS);
		END
	ELSE 	BEGIN
		INFXATOM('?();
		TDDLIST(ARGS, COL + 1, PARS + 1);
		INFXATOM('?));
		END;


EXPR TDDEXP (EXP, COL, PARS);
	BEGIN
	NEW TEM;
	TABTO(COL);
	IF FITSLINE(EXP, COL, PARS) THEN RETURN INFXEXPR(EXP, 0, 0);
	TEM ← GETGET(CAR EXP, 'TDDFUN);
	IF ¬NULL TEM THEN RETURN APPLY(TEM[2], <EXP, COL, PARS>);
NOAT; 	TDDFUNC(CAR EXP, COL, PARS);
	TDDARGS(CDR EXP, CURCOL(), PARS);
	END;


EXPR TDDFUNC (EXP, COL, PARS);
	BEGIN
	IF ATOM EXP THEN RETURN INFXATOM(EXP);
	INFXATOM('?();
	TDDEXP(EXP, COL + 1, PARS + 1);
	INFXATOM('?));
	END;


EXPR TDDLIST (EXP, COL, PARS);
	BEGIN
LOOP; 	IF NULL EXP THEN RETURN NIL;
	TDDEXP(CAR EXP, COL, PARS + 1);
	EXP ← CDR EXP;
	IF ¬NULL EXP THEN INFXATOM('?,);
	GO LOOP;
	END;


EXPR TDDINFX (EXP, COL, PARS);
	BEGIN
	NEW ARGS, INCR, OP;
	IF NULL CDR EXP | NULL CDDR EXP THEN RETURN INFX(EXP);
	OP ← CAR EXP;
	INCR ← FLATSIZE GETINFXNAM(CAR EXP);
	TDDEXP(EXP[2], COL, PARS);
	ARGS ← CDDR EXP;
LOOP; 	IF NULL ARGS THEN RETURN NIL;
	TERPRI();
	TABTO(COL);
	INFXATOM(OP);
	TDDEXP(CAR ARGS, COL + INCR, PARS);
	ARGS ← CDR ARGS;
	GO LOOP;
	END;


PUTPROP('PREC, 'TDDINFX, 'TDDFUN);


EXPR ALLFIT (LIST, WIDTH, RPARS);
	BEGIN
	IF NULL LIST THEN RETURN T;
LOOP; 	IF NULL CDR LIST THEN RETURN LEQ(FLATSIZE CAR LIST, WIDTH - RPARS);
	IF FLATSIZE CAR LIST ?*GREAT WIDTH THEN RETURN NIL;
	LIST ← CDR LIST;
	GO LOOP;
	END;


EXPR PRINL (X);
	IF NULL X THEN NIL
	ELSE IF CHRCT() ?*LESS FLATSIZE CAR X + 2 THEN 
		BEGIN
		TERPRI();
		PRINC '?	;
		PRINL(X);
		END
	ELSE 	BEGIN
		PRINS(CAR X);
		PRINL(CDR X);
		END;


EXPR PRINS (X);
	BEGIN
	PRINC X;
	PRINC '? ;
	END;


EXPR PRINTEXPR (EXP);
	BEGIN
	PRINTSUBEXPR(EXP, 1, 0);
	TERPRI();
	TERPRI();
	END;


EXPR PRINTLIST (LIST, LMARG, RPARS);
	BEGIN
	PRINC '?(;
	PRINTMEMBERS(LIST, LMARG + 1, RPARS + 1);
	PRINC '?);
	END;


EXPR PRINTMEMBERS (LIST, LMARG, RPARS);
	BEGIN
LOOP; 	IF NULL LIST THEN RETURN NIL;
	IF ATOM LIST THEN RETURN (
		BEGIN
		PRINC '? ?.? ;
		PRIN1 LIST;
		END);
	PRINTSUBEXPR(CAR LIST, LMARG, 
		IF NULL CDR LIST THEN RPARS + 1
		ELSE IF ATOM CDR LIST THEN RPARS + 4
		ELSE 0);
	LIST ← CDR LIST;
	GO LOOP;
	END;


EXPR PRINTSUBEXPR (SEXPR, LMARG, RPARS);
	BEGIN
	NEW TEM;
	TABTO(LMARG);
	IF ATOM SEXPR THEN RETURN PRIN1 SEXPR;
	IF ATOM CAR SEXPR & ¬NUMBERP CAR SEXPR THEN TEM ← GETGET(CAR SEXPR, 'PPROP);
	IF ¬NULL TEM THEN RETURN (
		LAMBDA (G0017); 
			G0017(SEXPR, LMARG, RPARS);
		(TEM[2]));
	IF LEQ(FLATSIZE SEXPR, CHRCT() - RPARS) THEN RETURN PRIN1 SEXPR;
	IF LEQ(FLATSIZE CAR SEXPR, 4) | ALLFIT(CDR SEXPR, CHRCT() - (2 + FLATSIZE CAR SEXPR), RPARS) THEN 
		RETURN (BEGIN
			PRINC '?(;
			PRIN1 CAR SEXPR;
			PRINC '? ;
			PRINTMEMBERS(CDR SEXPR, CURCOL(), 1 + RPARS);
			PRINC '?);
			END);
	PRINTLIST(SEXPR, LMARG, RPARS);
	END;


EXPR PRINTN (CHAR, NUM);
	BEGIN
	NEW NO;
	NO ← 1;
LOOP; 	IF NUM ?*LESS NO THEN RETURN NUM;
	PRINC CHAR;
	NO ← NO + 1;
	GO LOOP;
	END;


EXPR PRINTNOCRFUN (SEXPR, LMARG, RPARS);
	BEGIN
	IF LEQ(FLATSIZE SEXPR, CHRCT() - RPARS) THEN RETURN PRIN1 SEXPR;
	PRINC '?(;
	PRIN1 CAR SEXPR;
	PRINC '? ;
	PRINC SEXPR[2];
	PRINTMEMBERS(CDDR SEXPR, LMARG + 1, RPARS + 1);
	PRINC '?);
	END;


EXPR TABTO (COLNO);
	BEGIN
	IF CURCOL() ?*GREAT COLNO THEN TERPRI();
	PRINTN('?	, LSH(COLNO - CURCOL(), MINUS 3));
	PRINTN('? , COLNO - CURCOL());
	END;


PUTPROP('NOCR, 'PRINTNOCRFUN, 'PPROP);


FLAG('(ADDAXIOM ADDSCHEMA ADDTHEOREM DEFPROP GIVEAX GIVEPROOF GIVESCHM MAKETHM SETQ USEAX USESCHM), 'NOCR);


PROG2(PRECLIS?* ← 'IMPLIES CONS PRECLIS?*, MKPREC());


PROG2(PRECLIS?* ← 'EQUIVALENT CONS PRECLIS?*, MKPREC());


PRECSET('CMAPS, 'LESSP);


PRECSET('CONTAINED, 'LESSP);


PRECSET('INTERSECTION, 'CONTAINED);


PRECSET('MAPS, 'INTERSECTION);


PRECSET('MEMBER, 'LESSP);


PRECSET('PRODUCT, 'INTERSECTION);


PRECSET('UNION, 'CONTAINED);


PUTPROP('?&, '(NIL AND NIL), 'SWITCH?*);


PUTPROP('?⊂, '(NIL CONTAINED NIL), 'SWITCH?*);


PUTPROP('?=, '(?> EQUAL IMPLIES), 'SWITCH?*);


PUTPROP('?≡, '(NIL EQUIVALENT NIL), 'SWITCH?*);


PUTPROP('?∀, '(NIL FORALL NIL), 'SWITCH?*);


PUTPROP('?≥, '(NIL GEQ NIL), 'SWITCH?*);


PUTPROP('?∩, '(NIL INTERSECTION NIL), 'SWITCH?*);


PUTPROP('?→, '(?→ MAPS CMAPS), 'SWITCH?*);


PUTPROP('?⊃, '(NIL IMPLIES NIL), 'SWITCH?*);


PUTPROP('?≤, '(NIL LEQ NIL), 'SWITCH?*);


PUTPROP('?ε, '(NIL MEMBER NIL), 'SWITCH?*);


PUTPROP('?≠, '(NIL NEQ NIL), 'SWITCH?*);


PUTPROP('?⊗, '(NIL PRODUCT NIL), 'SWITCH?*);


PUTPROP('?∃, '(NIL THEREEXISTS NIL), 'SWITCH?*);


PUTPROP('?∪, '(NIL UNION NIL), 'SWITCH?*);


PUTPROP('ALL, 'FORALL, 'NEWNAM);


PUTPROP('EXISTS, 'THEREEXISTS, 'NEWNAM);


PUTPROP('EQU, 'EQUIVALENT, 'NEWNAM);


PUTPROP('GREATEQ, 'GEQ, 'NEWNAM);


PUTPROP('IMP, 'IMPLIES, 'NEWNAM);


PUTPROP('LESSEQ, 'LEQ, 'NEWNAM);


PUTPROP('MEM, 'MEMBER, 'NEWNAM);


LETTER(3);


REMPROP('LAMBDA, 'STAT);


REMPROP('GO, 'STAT);


REMPROP('STEP, 'DELIM);


REMPROP('DO, 'DELIM);


REMPROP('MAP, 'NEWFORM);


REMPROP('MAPLIST, 'NEWFORM);


REMPROP('MAPCAR, 'NEWFORM);


REMPROP('EXPLODE, 'NEWNAM);


IGLIST?* ← '(9 10 12 13 32);


PUTPROP('EXPR, 'PROCDEF, 'STAT);


LOGICALCONSTANTS ← '(TRUE FALSE);


QUANTIFIERS ← '(FORALL LAMBDA THEREEXISTS);


DDWIDTH ← 84;


FILEWIDTH ← 69;


IIIWIDTH ← 88;


IMLACWIDTH ← 80;


TTYWIDTH ← 71;


END.